T:Type, as:(T List), n:{0...||as||}, i:{0..n}. firstn(n;as)[i] = as[i]  T 

latex

Definitions	False, A, t  T, A  B, P  Q, , x:A. B(x), i  j , T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , Y, firstn(n;as), True, , ||as||, i  j < k, {i..j}, {i...j}, Unit, , P  Q, Dec(P),
Lemmas	int iseg wf, int seg wf, length wf1, le wf, ge wf, nat properties, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, nat wf, bnot wf, le int wf, assert wf, bool wf, lt int wf, length wf2, select wf, decidable int equal, select cons hd, firstn wf, select cons tl, length firstn, non neg length